home *** CD-ROM | disk | FTP | other *** search
/ Turnbull China Bikeride / Turnbull China Bikeride - Disc 1.iso / ARGONET / PD / PROGRAMMING / LCLINT2.SPK / test / test_b / c / spccluses5 < prev    next >
Text File  |  1996-08-28  |  937b  |  53 lines
  1. /*@-paramuse@*/ 
  2.  
  3. typedef struct 
  4. {
  5.   int id;
  6.   char *name;
  7. } *record;
  8.  
  9. /*@special@*/ record newrecord (void)
  10.   /*@defines result@*/
  11.   /*@post:isnull result->name@*/
  12. {
  13.   record r = (record) malloc (sizeof (*r));
  14.  
  15.   assert (r != NULL);
  16.   r->id = 3;
  17.   r->name = NULL;
  18.   return r;
  19. }
  20.  
  21. record createrecord (/*@only@*/ char *name)
  22. {
  23.   record r = newrecord ();
  24.   r->name = name;
  25.   return r;
  26. }
  27.  
  28. record createrecord2 (void)
  29. {
  30.   record r = newrecord ();
  31.   return r; /* 1. Null storage r->name derivable from return value: r */
  32. }
  33.  
  34. /*@special@*/ record newrecord2 (void)
  35.   /*@defines *result@*/
  36.   /*@post:observer result->name@*/
  37. {
  38.   record r = (record) malloc (sizeof (*r));
  39.  
  40.   assert (r != NULL);
  41.   r->id = 3;
  42.   r->name = NULL;
  43.   return r; /* 2. Non-observer storage r->name corresponds to storage ... */
  44. }
  45.  
  46. record createrecordx (void)
  47. {
  48.   record r = newrecord2 ();
  49.   return r; /* 3. Observer storage r->name reachable from observer return */
  50. }
  51.  
  52.  
  53.